(assert (or (bvslt #b01010011110 #b01010011110) (bvslt #b01010011110 #b01010011110) (bvslt #b01010011110 #b01010011110) (bvslt #b01010011110 #b01010011110)))
(assert (or (bvslt #b01010011110 #b01010011110) (bvslt #b01010011110 #b01010011110) (bvslt #b01010011110 #b01010011110) (bvslt #b01010011110 #b01010011110)))
(check-sat)
